Issue279-2.agda:20,7-12
⊥ !=< ⊤ of type Set
when checking that the inferred type of an application
  M.P ⊥ tt
matches the expected type
  M.P ⊤ tt
